/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.gui;

import java.awt.Color;
import java.awt.Font;
import java.awt.Graphics;
import java.awt.Graphics2D;
import java.awt.RenderingHints;
import java.awt.Toolkit;
import java.io.File;
import java.io.FileReader;
import java.io.FileWriter;
import java.io.IOException;
import java.util.EventListener;
import java.util.EventObject;

import javax.swing.JOptionPane;
import javax.swing.JTextArea;
import javax.swing.event.DocumentEvent;
import javax.swing.event.DocumentListener;
import javax.swing.event.EventListenerList;
import javax.swing.event.UndoableEditListener;
import javax.swing.text.DefaultHighlighter;
import javax.swing.text.Highlighter;
import javax.swing.undo.UndoManager;

import alloy.ast.Location;

// The LocatableTextArea is a Swing text area with additional
// operations, paticularly highlighting regions of text.

class LocatableTextArea extends JTextArea {
    private final LocDisplayer locDisplayer;
    private final EventListenerList listeners;
    private UndoManager undoManager;
    private File file;
    private String untitledName; // used to refer to file if there is no file name
    private int tabWidth;
    private boolean textModified = false;
    private final DocumentListener textDocumentListener;
    private final double windowsScaleFactor = (double)Toolkit.getDefaultToolkit().getScreenResolution() / 72.0;
    private Font selectedFont, renderedFont;
    private static boolean onWindows =
        (System.getProperty("os.name").toUpperCase().indexOf("WINDOWS") > -1);

    private DefaultHighlighter.DefaultHighlightPainter defaultPainter;

    LocatableTextArea() {

        locDisplayer = new LocDisplayer(this);
	file = null;
	untitledName = null;

        undoManager = new UndoManager();
        getDocument().addUndoableEditListener(
            (UndoableEditListener)AlloySwingUtilities.listener(undoManager));

        textDocumentListener = getDocumentListener();
        getDocument().addDocumentListener(
            (DocumentListener)AlloySwingUtilities.listener(textDocumentListener));

        listeners = new EventListenerList();

        defaultPainter = new DefaultHighlighter.DefaultHighlightPainter(Color.green);

    }

    public void paintComponent(Graphics g) {
        //  feeble attempt to fix "ugly" fonts on windows
        if (onWindows) {
            if (g instanceof Graphics2D) {
                Graphics2D g2 = (Graphics2D)g;
                if (getFont().getSize() > 18) {
                    g2.addRenderingHints(
                        new RenderingHints(
                            RenderingHints.KEY_ANTIALIASING,
                            RenderingHints.VALUE_ANTIALIAS_ON));
                }
                else {
                    g2.addRenderingHints(
                        new RenderingHints(
                            RenderingHints.KEY_ANTIALIASING,
                            RenderingHints.VALUE_ANTIALIAS_OFF));
                }

                super.paintComponent(g2);
                g2.dispose();
            }
            else {
                super.paintComponent(g);
            }
        }
        else {
            super.paintComponent(g);
        }
    }

    public void setFont(Font f) {
        if (onWindows) {
            if (!f.equals(selectedFont)) {
                renderedFont = calculateRenderedFont(f);
                selectedFont = f;
                super.setFont(renderedFont);
            }
        }
        else {
            super.setFont(f);
        }
    }

    private Font calculateRenderedFont(Font f) {
        return new Font(f.getName(), Font.PLAIN, (int)Math.round(f.getSize() * windowsScaleFactor));
    }

    public String addLoc(Location loc, Highlighter.HighlightPainter painter) {
        return locDisplayer.showLoc(loc, painter, false);
    }

    public String showLoc(Location loc, Highlighter.HighlightPainter painter) {
        clearLocs();
        return locDisplayer.showLoc(loc, painter, true);
    }

    public void showLoc(Location loc) {
        showLoc(loc, defaultPainter);
    }

    public void clearLocs() {
        locDisplayer.clearHighlights();
    }

    String getFileName() {
	return file == null ? null : file.getName();
    }

    String getFilePath() {
	return file == null ? null : file.getAbsolutePath();
    }

    String getFileString() {
	return 
	    (file == null ? untitledName : getFileName()) +
	    (isEditable() ? "" : " (Read-Only)") +
	    (textModified && (file != null) ? "*" : "");
    }

    void setUntitledName(String name) {
	untitledName = name;
    }

    public void setTabSize(int tabSize_) {
        tabWidth = tabSize_;
        super.setTabSize(tabWidth);
        updateUI();
    }

    /*
     * File operations
     * 
     * All of these following methods return true on success, and false
     * if there was an error. Note that an ``error'' can simply mean that
     * the user didn't confirm the operation.
     */

    boolean saveFile() {
        if (file == null) return false;

	if (!textModified) return true;

        return writeFile(file);
    }

    boolean saveFileAs(File file_) {
	if (file_.exists()) {
	    int selection =
		JOptionPane.
		showConfirmDialog(
				  getTopLevelAncestor(),
				  "The file you have selected exists; are you sure\n"
				  + "that you want to overwrite it?",
				  "File Exists",
				  JOptionPane.YES_NO_OPTION,
				  JOptionPane.WARNING_MESSAGE);
	    
	    if (selection == JOptionPane.NO_OPTION)
		return false;
	}
	file = file_;

        return writeFile(file);
    }

    boolean reloadFile() {
        if (file == null) {
            JOptionPane.showMessageDialog(
                getTopLevelAncestor(),
                "You need to open a file before you can reload it.",
                "Reload Error",
                JOptionPane.ERROR_MESSAGE);
            return false;
        }
        else {
            return readFile(file, false);
        }

    }

    boolean saveFileCopyAs(File file_) {
	if (file_.exists()) {
	    int selection =
		JOptionPane.
		showConfirmDialog(
				  getTopLevelAncestor(),
				  "The file you have selected exists; are you sure\n"
				  + "that you want to overwrite it?",
				  "File Exists",
				  JOptionPane.YES_NO_OPTION,
				  JOptionPane.WARNING_MESSAGE);
	    
	    if (selection == JOptionPane.NO_OPTION)
		return false;
	}
	
	FileWriter writer = null;
	
	try {
	    writer = new FileWriter(file_);
	    write(writer);
	}
	catch (IOException exception) {
	    JOptionPane.showMessageDialog(
					  getTopLevelAncestor(),
					  "Unable to write to file: " + file_.getAbsolutePath(),
					  "Save Copy",
					  JOptionPane.ERROR_MESSAGE);
	    return false;
	}
	finally {
	    if (writer != null) {
		try {
		    writer.close();
		}
		catch (IOException ex) {
		    return false;
		}
	    }
	}
	
        return true;
    }

    /* End file operations. */

    /**
     * undo if able
     */
    void undo() {
        if (undoManager.canUndo()) {
            undoManager.undo();
        }
    }

    /**
     * redo if able
     */
    void redo() {
        if (undoManager.canRedo()) {
            undoManager.redo();
        }
    }

    boolean readFile(String fileName_) {
	return readFile(fileName_, true);
    }

    boolean readFile(File file_) {
        return readFile(file_, true);
    }

    boolean readFile(String fileName_, boolean checkMod) {
	return readFile(new File(fileName_), checkMod);
    }

    /**
     * Load the specified file into the Alloy model display.
     * Normally invoked when the user chooses File|Open or
     * File|Reload, but can also be invoked when the user
     * clicks an AST node in the Evaluator and the Alloy spec
     * from which that node was compiled is in another file --
     * in that case {@link LocDisplayer} calls this routine
     * to bring that file into the model display so it can
     * highlight the spec text corresponding to the AST node.
     * Returns true on success. If checkMod is false, then no
     * check for a modified buffer is performed.
     */
    boolean readFile(File file_, boolean checkMod) {
        if (textModified && checkMod) {
            if (!checkConfirmOperation())
                return false;
        }

        FileReader reader = null;

        try {
            reader = new FileReader(file_);
            read(reader, null);
            getDocument().addDocumentListener(
                (DocumentListener)AlloySwingUtilities.listener(textDocumentListener));
            undoManager = new UndoManager();
            getDocument().addUndoableEditListener(
                (UndoableEditListener)AlloySwingUtilities.listener(undoManager));
	    file = file_;

        }
        catch (IOException exception) {
            JOptionPane.showMessageDialog(
                getTopLevelAncestor(),
                "Unable to read from file: " + file_.getAbsolutePath(),
                "Open",
                JOptionPane.ERROR_MESSAGE);
            return false;
        }
        finally {
            if (reader != null) {
                try {
                    reader.close();
                }
                catch (IOException ex) {
                    return false;
                }
            }
        }

	fireFileChanged(file_);

        textModified = false;
        setTabSize(tabWidth);

        return true;
    }

    boolean writeFile(File file_) {
        // Let's write it to disk now.
        FileWriter writer = null;

        try {
            writer = new FileWriter(file_);
            write(writer);
        }
        catch (IOException exception) {
            JOptionPane.showMessageDialog(
                getTopLevelAncestor(),
                "Unable to write to file: " + file_,
                "Save",
                JOptionPane.ERROR_MESSAGE);
            return false;
        }
        finally {
            if (writer != null) {
                try {
                    textModified = false;
                    fireFileSaved(file_);
                    writer.close();
                }
                catch (IOException ex) {
                    return false;
                }
            }
        }

        return true;
    }

    // checkConfirmOperation () checks if the text has been modified; if so,
    // it prompts the user to confirm his actions.
    // Return: true if the operation should continue, and false otherwise.
    public boolean checkConfirmOperation() {
        int selection;
        boolean retval = true;

        if (textModified == true) {
            selection =
                JOptionPane.showConfirmDialog(
                    getTopLevelAncestor(),
                    getFileString()
                        + " has not been saved.\n"
                        + "Are you sure you want to continue with this operation?",
                    "Document Not Saved",
                    JOptionPane.YES_NO_OPTION,
                    JOptionPane.WARNING_MESSAGE);

            if (selection == JOptionPane.NO_OPTION)
                retval = false;
        }

        return retval;
    }

    DocumentListener getDocumentListener() {
        return new DocumentListener() {
            public void insertUpdate(DocumentEvent e) {
                textModifiedHandler();
            }

            public void removeUpdate(DocumentEvent e) {
                textModifiedHandler();
            }

            public void changedUpdate(DocumentEvent e) {
                textModifiedHandler();
            }

            private void textModifiedHandler() {
                if (textModified == false) {
                    textModified = true;
                    fireTextChanged();
                }
            }
        };
    }

    /*
     * Managers for listener lists.
     */

    public void addTextChangedListener(TextChangedListener listener) {
        listeners.add(TextChangedListener.class, listener);
    }

    public void removeTextChangedListener(TextChangedListener listener) {
        listeners.remove(TextChangedListener.class, listener);
    }

    void fireTextChanged() {
        TextChangedEvent event = new TextChangedEvent(this);

        Object[] listenerArray = listeners.getListenerList();

        for (int i = listenerArray.length - 2; i >= 0; i -= 2) {
            if (listenerArray[i] == TextChangedListener.class) {
                ((TextChangedListener)listenerArray[i + 1]).textChanged(event);
            }
        }
    }

    public void addFileChangedListener(FileChangedListener listener) {
        listeners.add(FileChangedListener.class, listener);
    }

    public void removeFileChangedListener(FileChangedListener listener) {
        listeners.remove(FileChangedListener.class, listener);
    }

    void fireFileChanged(File file) {
        FileChangedEvent event = new FileChangedEvent(this, file);

        Object[] listenerArray = listeners.getListenerList();

        for (int i = listenerArray.length - 2; i >= 0; i -= 2) {
            if (listenerArray[i] == FileChangedListener.class) {
                ((FileChangedListener)listenerArray[i + 1]).fileChanged(event);
            }
        }
    }

    public void addFileSavedListener(FileSavedListener listener) {
        listeners.add(FileSavedListener.class, listener);
    }

    public void removeFileSavedListener(FileSavedListener listener) {
        listeners.remove(FileSavedListener.class, listener);
    }

    void fireFileSaved(File file) {
        FileSavedEvent event = new FileSavedEvent(this, file);

        Object[] listenerArray = listeners.getListenerList();

        for (int i = listenerArray.length - 2; i >= 0; i -= 2) {
            if (listenerArray[i] == FileSavedListener.class) {
                ((FileSavedListener)listenerArray[i + 1]).fileSaved(event);
            }
        }
    }

    /*
     * Inner classes
     */

    public class TextChangedEvent extends EventObject {
        public TextChangedEvent(Object source) {
            super(source);
        }
    }

    public class FileChangedEvent extends EventObject {
        File file;

        public FileChangedEvent(Object source, File file_) {
            super(source);
            file = file_;
        }

        public File getFile() {
            return file;
        }
    }

    public class FileSavedEvent extends EventObject {
        File file;

        public FileSavedEvent(Object source, File file_) {
            super(source);
            file = file_;
        }

        public File getFile() {
            return file;
        }
    }

    public interface TextChangedListener extends EventListener {
        public void textChanged(TextChangedEvent event);
    }

    public interface FileChangedListener extends EventListener {
        public void fileChanged(FileChangedEvent event);
    }

    public interface FileSavedListener extends EventListener {
        public void fileSaved(FileSavedEvent event);
    }

}
